#ifndef MCMAS_MAIN_HEADER
#define MCMAS_MAIN_HEADER

#define NAME "mcmas"
#define URL "http://www.cs.ucl.ac.uk/staff/f.raimondi/MCMAS/"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <setjmp.h>
#include <string>
#include <iostream>
#include <fstream>
#include <vector>
#include <map>
#include <set>
#include <algorithm>
#include <cctype>
#include <ctime>
#include "types.hh"
#include "utilities.hh"
#include "mcmas-driver.hh"
#include "cuddObj.hh"
#include "dddmpInt.h"
#include <sys/types.h>
#include <unistd.h>


#define MAXINISTATES 100
#define MAXTRANSITIONS 100
#define MAXSTACKDEPTH 100

typedef std::vector<modal_formula> modal_formula_vector;
typedef std::pair<modal_formula *, modal_formula *> modal_formula_p_pair;
typedef std::vector<modal_formula_p_pair> modal_formula_p_pair_vector;

map<string, basic_agent *> *is_agents;
vector<basic_agent *> *agents;
map<string, bool_expression *> *is_evaluation;
bool_expression *is_istates = NULL;
map<string, set<string> > *is_groups;
modal_formula_vector *is_formulae;
modal_formula_p_pair_vector *bmc_formulae;
modal_formula_p_pair_vector *bmc_false_formulae;

vector<fairness_expression *> *is_fairness;
int obsvars_bdd_length;
int envars_bdd_length;

map<string, int> options;
// A map to store global options, e.g. verbosity, etc.
// 'verbosity' -> 0 (default) -- 5

string cex_prefix; // Destination directory for counterexamples
string initbddfile;

bool global_consistency_check();

Cudd *bddmgr; // The manager
BDDvector *v; // Local states
BDDvector *vRT;
ADDvector *addv;
BDDvector *pv; // "Next" local states
ADDvector *addpv;
BDDvector *a; // Actions
BDD andprot; //Joint protocol
BDD preRT; // Temporal trans with actions
BDD trans;
BDD RT; // Temporal transition
BDD reach; // Reachable states
BDD reachRT;
bool calReachRT;
map<string, BDD> er; // Epistemic Relations
map<string, BDD> deor; // Deontic relation
map<string, BDD> gm; // For "Everybody in a group knows".
map<string, BDD> deogm; // Deontic group modalities
map<string, BDD> distgm; // Distributed knowledge modalities
BDD fair_reach;
BDDvector *vevol, *vprot;
BDD in_st; // Initial States
BDD* bddOne;

vector<vector<int> *> *countex; // For counterexamples
map<int, BDD *> *idbdd; // Map state id -> bdd (for counterexamples again)
int scount; // a global counter for counterexamples.

vector<vector<transition *> *> *cextr; // instead of state id, counterexample with transitions

bool need_epistemic;
bool need_deontic;
bool need_common_knowledge;
bool need_deontic_knowledge;
bool need_distributed_knowledge;
bool no_kbar;
int one_shot_depth;

modal_formula * atomic_k_bar_formula;

map<string, BDD> *symmetry_cache;
map<string, string> *symmetry_atom_cache;

void setup(int argc, char* argv[]);
void simulate(void);
void experiment_0(void);
void experiment_1(void);
void experiment_2(void);
void experiment_3(void);
void experiment_4(void);
void experiment_5_Master(void);
void experiment_5_Slave(void);
void experiment_6(void);
void check_formulae(void);
void check_formulae_BMC(void);

void print_help(void);
void print_banner(void);
void print_ispl_code(void);
void print_state(BDD state, BDDvector v);
string state_to_str(BDD state, BDDvector v);
bool find_same_state(map<string, int> *statehash, string state);
bool is_valid_state(BDD state, BDDvector v);
void print_action(BDD state, BDDvector a);
void print_action_1(BDD state, BDDvector a);
bool is_valid_action(BDD state, BDDvector a);
BDD append_variable_BDDs(BDD a);
void build_cex(modal_formula *f, int i);

#endif /* MCMAS_MAIN_HEADER */
